[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
data asm specification
afs
using afs-pre,
error-class
,
eraseblock
procedures afs_drop_nlink# nat : dir-heap × file-heap nonfunctional ;
afs_inc_nlink# nat : dir-heap × file-heap nonfunctional ;
afs_check_commit# dir-heap × file-heap : error : bool nondeterministic;
afs_format# nat × bool × nat × metadata : dir-heap : file-heap × bool × error nondeterministic;
afs_recovery# bool : dir-heap × file-heap : bool × error nondeterministic;
afs_sync# dir-heap × file-heap : : bool × error nondeterministic;
afs_fsync# inode × bool × dir-heap × file-heap : : bool × error nondeterministic;
afs_fsyncdir# inode × bool × dir-heap × file-heap × bool : : error nondeterministic;
afs_inode_sync# inode : dir-heap × file-heap nonfunctional ;
afs_lookup# nat × dir-heap × file-heap × bool : dentry × error nonfunctional nondeterministic;
afs_create_ino# nat × metadata × nat : dentry × error × dir-heap × file-heap nonfunctional ;
afs_create# metadata : inode × inode × dentry × error × dir-heap × file-heap : bool nondeterministic;
afs_unlink# : inode × inode × dentry × error × dir-heap × file-heap : bool nondeterministic;
afs_mkdir_ino# nat × metadata × nat : dentry × error × dir-heap nonfunctional ;
afs_mkdir# metadata : inode × inode × dentry × error × dir-heap × file-heap : bool nondeterministic;
afs_rmdir# : inode × inode × dentry × error × dir-heap × file-heap : bool nondeterministic;
afs_link# dentry : inode × inode × dentry × error × dir-heap × file-heap : bool nondeterministic;
afs_rename# : inode × inode × inode × inode × dentry × dentry × error × dir-heap × file-heap : bool nondeterministic;
afs_readpage# inode × nat × dir-heap × file-heap × bool : buffer × error nonfunctional nondeterministic;
afs_writepage# inode × nat × buffer × dir-heap : error × file-heap : bool nondeterministic;
afs_readdir# inode × dir-heap × file-heap × bool : stringset × error nonfunctional nondeterministic;
afs_evict# inode × bool : error × dir-heap × file-heap nonfunctional ;
afs_truncate# nat × nat : buffer-opt × inode × bool × error × dir-heap × file-heap × bool nonfunctional nondeterministic;
afs_truncate_internal# nat × nat : inode × buffer-opt × nat × nat × bool × error × dir-heap × file-heap : bool nondeterministic;
afs_iget# nat × dir-heap × file-heap × bool : inode × error nonfunctional nondeterministic;
afs_write_inode# inode : error × dir-heap × file-heap : bool nondeterministic;
variables NS : nat-set flexible;
N : nat flexible;
SIZE : nat flexible;
PAGENO : nat flexible;
OFFSET : nat flexible;
END : nat flexible;
DENT : dentry flexible;
DENT0 : dentry flexible;
OLD_INO : nat flexible;
NEW_INO : nat flexible;
DENT_INO : nat flexible;
DENTRY_INO : nat flexible;
OLD_DENT : dentry flexible;
NEW_DENT : dentry flexible;
INO : nat flexible;
P_INO : nat flexible;
C_INO : nat flexible;
P_INODE : inode flexible;
C_INODE : inode flexible;
FILES : file-heap flexible;
DIRS : dir-heap flexible;
ERR : error flexible;
MD : metadata flexible;
PBUF : buffer flexible;
INODE : inode flexible;
NAMES : stringset flexible;
NAMES0 : stringset flexible;
CONTENT : file-content flexible;
MODIFIED : bool flexible;
ISDATASYNC : bool flexible;
IDENTITY : bool flexible;
OVERWRITE : bool flexible;
OLD_INODE : inode flexible;
NEW_INODE : inode flexible;
DENTRY_INODE : inode flexible;
OLD_DENT_INODE : inode flexible;
NEW_DENT_INODE : inode flexible;
OLD_PARENT_INODE : inode flexible;
NEW_PARENT_INODE : inode flexible;
OLD_CHILD_INODE : inode flexible;
NEW_CHILD_INODE : inode flexible;
PBUF-OPT : buffer-opt flexible;
ASYNCED : bool flexible;
asynced : bool;
DOSYNC : bool flexible;
state variables DIRS : dir-heap flexible;
FILES : file-heap flexible;
ASYNCED : bool flexible;
initialization procedure afs_format#
if ERR = ESUCCESS
sequential
invariants afs-cons : ⊦ afs-cons(DIRS, FILES);
crash predicate DIRS = DIRS` \ orphans(DIRS`, FILES`) ∧ FILES = FILES` \ orphans(DIRS`, FILES`)
with crash-neutrality
synchronized predicate
ASYNCED
recovery procedure afs_recovery#
if ERR = ESUCCESS
declarations drop-nlink
: afs_drop_nlink#(INO; DIRS, FILES)
{if INO ∈ DIRS then DIRS[INO].nlink := DIRS[INO].nlink - 1; if INO ∈ FILES then FILES[INO].nlink := FILES[INO].nlink - 1}
;
inc-nlink
: afs_inc_nlink#(INO; DIRS, FILES)
{if INO ∈ DIRS then DIRS[INO].nlink := DIRS[INO].nlink + 1; if INO ∈ FILES then FILES[INO].nlink := FILES[INO].nlink + 1}
;
check-commit:
afs_check_commit#(DIRS, FILES; ERR; ASYNCED)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR); choose bv with true in ASYNCED := bv}
}
format:
afs_format#(N, DOSYNC, SIZE, MD; DIRS; FILES, ASYNCED, ERR)
precondition SIZE = LEB_SIZE;
postcondition true;
{if SIZE = LEB_SIZE
then { {DIRS := ∅, FILES := ∅; DIRS := DIRS ++ ROOT_INO; DIRS[ROOT_INO] := mkdir(0, MD, 0, 0, ∅); ASYNCED := true; ERR := ESUCCESS}
or {DIRS := ?, FILES := ?, ASYNCED := ?; fail#(; ; ERR)}}
else abort
}
recovery:
afs_recovery#(DOSYNC; DIRS, FILES; ASYNCED, ERR)
precondition true;
postcondition true;
{{ASYNCED := true, ERR := ESUCCESS or {DIRS := ?, FILES := ?, ASYNCED := ?; fail#(; ; ERR)}}
}
sync:
afs_sync#(DIRS, FILES; ; ASYNCED, ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR); ASYNCED := ERR = ESUCCESS}
}
fsync:
afs_fsync#(INODE, ISDATASYNC, DIRS, FILES; ; ASYNCED, ERR)
precondition valid-file-inode(INODE, DIRS, FILES);
postcondition true;
{if valid-file-inode(INODE, DIRS, FILES) then {fail_or_success#(; ; ERR); choose bv with true in ASYNCED := bv} else abort
}
fsyncdir:
afs_fsyncdir#(INODE, ISDATASYNC, DIRS, FILES, ASYNCED; ; ERR)
precondition true;
postcondition true;
{fail_or_success#(; ; ERR)
}
internal-inode-sync
: afs_inode_sync#(INODE; DIRS, FILES)
{let INO = INODE.ino
in if INO ∈ FILES
then {FILES[INO].size := INODE.size; FILES[INO].meta := INODE.meta}
else if INO ∈ DIRS then DIRS[INO].meta := INODE.meta
}
;
lookup:
afs_lookup#(P_INO, DIRS, FILES, ASYNCED; DENT, ERR)
precondition pre-lookup(P_INO, DENT, DIRS, FILES);
postcondition true;
{if pre-lookup(P_INO, DENT, DIRS, FILES)
then { if DENT.name ∈ DIRS[P_INO].entries
then {DENT := mkdentry(DENT.name, DIRS[P_INO].entries[DENT.name]); ERR := ESUCCESS}
else {DENT := negdentry(DENT.name); ERR := ENOENT}
or fail#(; ; ERR)}
else abort
}
create-ino
: afs_create_ino#(P_INO, MD, INO; DENT, ERR, DIRS, FILES)
{DIRS[P_INO].entries[DENT.name] := INO; DIRS[P_INO].size := DIRS[P_INO].size + 1; FILES := FILES ++ INO;
FILES[INO] := mkfile(0, MD, 1, ∅); DENT := mkdentry(DENT.name, INO); ERR := ESUCCESS
}
;
create:
afs_create#(MD; P_INODE, C_INODE, DENT, ERR, DIRS, FILES; ASYNCED)
precondition pre-create(P_INODE, DENT, MD, DIRS, FILES);
postcondition true;
{if pre-create(P_INODE, DENT, MD, DIRS, FILES)
then { {choose INO with ¬ INO ∈ DIRS ∧ ¬ INO ∈ FILES ∧ INO ≠ 0 in afs_create_ino#(P_INODE.ino, MD, INO; DENT, ERR, DIRS, FILES);
afs_inode_sync#(P_INODE; DIRS, FILES); P_INODE := getinode(P_INODE.ino, DIRS, FILES);
C_INODE := getinode(DENT.ino, DIRS, FILES)}
or fail#(; ; ERR);
ASYNCED := ?}
else abort
}
unlink:
afs_unlink#(; P_INODE, C_INODE, DENT, ERR, DIRS, FILES; ASYNCED)
precondition pre-unlink(P_INODE, C_INODE, DENT, DIRS, FILES);
postcondition true;
{if pre-unlink(P_INODE, C_INODE, DENT, DIRS, FILES)
then { let P_INO = P_INODE.ino
in {DIRS[P_INO].entries := DIRS[P_INO].entries -- DENT.name; DIRS[P_INO].size := DIRS[P_INO].size - 1;
let INO = DENT.ino in afs_drop_nlink#(INO; DIRS, FILES); DENT := negdentry(DENT.name);
afs_inode_sync#(P_INODE; DIRS, FILES); afs_inode_sync#(C_INODE; DIRS, FILES);
P_INODE := getinode(P_INODE.ino, DIRS, FILES); C_INODE := getinode(C_INODE.ino, DIRS, FILES); ERR := ESUCCESS}
or fail#(; ; ERR);
ASYNCED := ?}
else abort
}
mkdir-ino
: afs_mkdir_ino#(P_INO, MD, INO; DENT, ERR, DIRS)
{DIRS[P_INO].entries[DENT.name] := INO; DIRS[P_INO].size := DIRS[P_INO].size + 1; DIRS[P_INO].nsubdirs := DIRS[P_INO].nsubdirs + 1;
DIRS := DIRS ++ INO; DIRS[INO] := mkdir(0, MD, 1, 0, ∅); DENT := mkdentry(DENT.name, INO); ERR := ESUCCESS
}
;
mkdir:
afs_mkdir#(MD; P_INODE, C_INODE, DENT, ERR, DIRS, FILES; ASYNCED)
precondition pre-mkdir(P_INODE, DENT, MD, DIRS, FILES);
postcondition true;
{if pre-mkdir(P_INODE, DENT, MD, DIRS, FILES)
then { {choose INO with ¬ INO ∈ DIRS ∧ ¬ INO ∈ FILES ∧ INO ≠ 0 in afs_mkdir_ino#(P_INODE.ino, MD, INO; DENT, ERR, DIRS);
afs_inode_sync#(P_INODE; DIRS, FILES); P_INODE := getinode(P_INODE.ino, DIRS, FILES);
C_INODE := getinode(DENT.ino, DIRS, FILES)}
or fail#(; ; ERR);
ASYNCED := ?}
else abort
}
rmdir:
afs_rmdir#(; P_INODE, C_INODE, DENT, ERR, DIRS, FILES; ASYNCED)
precondition pre-rmdir(P_INODE, C_INODE, DENT, DIRS, FILES);
postcondition true;
{if pre-rmdir(P_INODE, C_INODE, DENT, DIRS, FILES)
then { let P_INO = P_INODE.ino
in {DIRS[P_INO].entries := DIRS[P_INO].entries -- DENT.name; DIRS[P_INO].size := DIRS[P_INO].size - 1;
DIRS[P_INO].nsubdirs := DIRS[P_INO].nsubdirs - 1; let INO = DENT.ino in afs_drop_nlink#(INO; DIRS, FILES);
DENT := negdentry(DENT.name); afs_inode_sync#(P_INODE; DIRS, FILES); afs_inode_sync#(C_INODE; DIRS, FILES);
P_INODE := getinode(P_INODE.ino, DIRS, FILES); C_INODE := getinode(C_INODE.ino, DIRS, FILES); ERR := ESUCCESS}
or fail#(; ; ERR);
ASYNCED := ?}
else abort
}
link:
afs_link#(OLD_DENT; P_INODE, C_INODE, NEW_DENT, ERR, DIRS, FILES; ASYNCED)
precondition pre-link(P_INODE, C_INODE, OLD_DENT, NEW_DENT, DIRS, FILES);
postcondition true;
{if pre-link(P_INODE, C_INODE, OLD_DENT, NEW_DENT, DIRS, FILES)
then { let P_INO = P_INODE.ino
in {DIRS[P_INO].entries[NEW_DENT.name] := OLD_DENT.ino; DIRS[P_INO].size := DIRS[P_INO].size + 1;
let INO = OLD_DENT.ino in afs_inc_nlink#(INO; DIRS, FILES); NEW_DENT := mkdentry(NEW_DENT.name, OLD_DENT.ino);
afs_inode_sync#(P_INODE; DIRS, FILES); afs_inode_sync#(C_INODE; DIRS, FILES);
P_INODE := getinode(P_INODE.ino, DIRS, FILES); C_INODE := getinode(OLD_DENT.ino, DIRS, FILES); ERR := ESUCCESS}
or fail#(; ; ERR);
ASYNCED := ?}
else abort
}
renam:
afs_rename#(; OLD_PARENT_INODE, NEW_PARENT_INODE, OLD_CHILD_INODE, NEW_CHILD_INODE, OLD_DENT, NEW_DENT, ERR, DIRS, FILES; ASYNCED)
precondition pre-rename(OLD_PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_PARENT_INODE, NEW_DENT, NEW_CHILD_INODE, DIRS, FILES);
postcondition true;
{if pre-rename(OLD_PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_PARENT_INODE, NEW_DENT, NEW_CHILD_INODE, DIRS, FILES)
then { let OLD_INO = OLD_PARENT_INODE.ino, NEW_INO = NEW_PARENT_INODE.ino, OVERWRITE = NEW_DENT.dentry?
in let IDENTITY = OLD_INO = NEW_INO ∧ NEW_DENT = OLD_DENT
in {DIRS[OLD_INO].entries := DIRS[OLD_INO].entries -- OLD_DENT.name;
if ¬ IDENTITY
then {DIRS[OLD_INO].size := DIRS[OLD_INO].size - 1;
if OLD_DENT.ino ∈ DIRS then DIRS[OLD_INO].nsubdirs := DIRS[OLD_INO].nsubdirs - 1};
DIRS[NEW_INO].entries[NEW_DENT.name] := OLD_DENT.ino;
if OVERWRITE ∧ ¬ IDENTITY then let INO = NEW_DENT.ino in afs_drop_nlink#(INO; DIRS, FILES);
if ¬ OVERWRITE
then {DIRS[NEW_INO].size := DIRS[NEW_INO].size + 1;
if OLD_DENT.ino ∈ DIRS then DIRS[NEW_INO].nsubdirs := DIRS[NEW_INO].nsubdirs + 1};
NEW_DENT := mkdentry(NEW_DENT.name, OLD_DENT.ino); OLD_DENT := negdentry(OLD_DENT.name);
afs_inode_sync#(OLD_PARENT_INODE; DIRS, FILES); afs_inode_sync#(NEW_PARENT_INODE; DIRS, FILES);
if OVERWRITE
then {afs_inode_sync#(NEW_CHILD_INODE; DIRS, FILES);
NEW_CHILD_INODE := getinode(NEW_CHILD_INODE.ino, DIRS, FILES)};
OLD_PARENT_INODE := getinode(OLD_PARENT_INODE.ino, DIRS, FILES);
NEW_PARENT_INODE := getinode(NEW_PARENT_INODE.ino, DIRS, FILES); ERR := ESUCCESS}
or fail#(; ; ERR);
ASYNCED := ?}
else abort
}
readpage:
afs_readpage#(INODE, PAGENO, DIRS, FILES, ASYNCED; PBUF, ERR)
precondition pre-readpage(INODE, PAGENO, PBUF, DIRS, FILES);
postcondition true;
{if pre-readpage(INODE, PAGENO, PBUF, DIRS, FILES)
then { {if PAGENO ∈ FILES[INODE.ino].content then PBUF := FILES[INODE.ino].content[PAGENO] else PBUF := zeropage; ERR := ESUCCESS}
or fail#(; ; ERR)}
else abort
}
writepage:
afs_writepage#(INODE, PAGENO, PBUF, DIRS; ERR, FILES; ASYNCED)
precondition pre-writepage(INODE, PAGENO, PBUF, DIRS, FILES);
postcondition true;
{if pre-writepage(INODE, PAGENO, PBUF, DIRS, FILES)
then {{FILES[INODE.ino].content[PAGENO] := PBUF; ERR := ESUCCESS} or fail#(; ; ERR); ASYNCED := ?}
else abort
}
readdir:
afs_readdir#(INODE, DIRS, FILES, ASYNCED; NAMES, ERR)
precondition pre-readdir(INODE.ino, DIRS, FILES);
postcondition true;
{if pre-readdir(INODE.ino, DIRS, FILES)
then {{NAMES := dom DIRS[INODE.ino].entries; ERR := ESUCCESS} or {choose NAMES0 with true in NAMES := NAMES0; fail#(; ; ERR)}}
else abort
}
evict:
afs_evict#(INODE, ASYNCED; ERR, DIRS, FILES)
precondition pre-evict(INODE, DIRS, FILES);
postcondition true;
{if pre-evict(INODE, DIRS, FILES)
then {ERR := ESUCCESS;
let INO = INODE.ino
in if INO ∈ DIRS then if DIRS[INO].nlink = 0 then DIRS := DIRS -- INO else if FILES[INO].nlink = 0 then FILES := FILES -- INO}
else abort
}
truncate:
afs_truncate#(N, PAGENO; PBUF-OPT, INODE, MODIFIED, ERR, DIRS, FILES, ASYNCED)
precondition pre-truncate(INODE, N, PAGENO, PBUF-OPT, DIRS, FILES);
postcondition true;
{if pre-truncate(INODE, N, PAGENO, PBUF-OPT, DIRS, FILES)
then let OFFSET = 0, SIZE = 0
in afs_truncate_internal#(N, PAGENO; INODE, PBUF-OPT, OFFSET, SIZE, MODIFIED, ERR, DIRS, FILES; ASYNCED)
else abort
}
truncate-internal
: afs_truncate_internal#(N, PAGENO; INODE, PBUF-OPT, OFFSET, SIZE, MODIFIED, ERR, DIRS, FILES; ASYNCED)
{ let INO = INODE.ino, CONTENT = FILES[INODE.ino].content, PBUF = ?
in {OFFSET := INODE.size % VFS_PAGE_SIZE, SIZE := min(N, INODE.size);
MODIFIED := INODE.size ≤ N ∧ OFFSET ≠ 0 ∧ (PAGENO ∈ CONTENT ∨ PBUF-OPT.some?);
if MODIFIED
then {if PBUF-OPT.some? then PBUF := PBUF-OPT.buf else PBUF := FILES[INO].content[PAGENO];
PBUF := fill(PBUF, zero, OFFSET, VFS_PAGE_SIZE - OFFSET); CONTENT[PAGENO] := PBUF; PBUF-OPT := some(PBUF)};
FILES[INO].content := CONTENT upto SIZE;
let NEW_INODE = INODE in {NEW_INODE.size := N; afs_inode_sync#(NEW_INODE; DIRS, FILES)};
INODE := getinode(INODE.ino, DIRS, FILES); ERR := ESUCCESS}
or fail#(; ; ERR);
ASYNCED := ?
}
;
iget:
afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR)
precondition pre-iget(INO, DIRS, FILES);
postcondition true;
{if pre-iget(INO, DIRS, FILES) then {{INODE := getinode(INO, DIRS, FILES); ERR := ESUCCESS} or fail#(; ; ERR)} else abort
}
write_inode:
afs_write_inode#(INODE; ERR, DIRS, FILES; ASYNCED)
precondition pre-write-inode(INODE, DIRS, FILES);
postcondition true;
{if pre-write-inode(INODE, DIRS, FILES)
then { {if INODE.directory
then DIRS[INODE.ino].meta := INODE.meta
else {FILES[INODE.ino].meta := INODE.meta; FILES[INODE.ino].size := INODE.size};
ERR := ESUCCESS}
or fail#(; ; ERR);
ASYNCED := ?}
else abort
}
end data asm specification